COMMENT ⊗   VALID 00010 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	FOLMRG is a program for reformating FOL input and output files.  It has 
C00004 00003	MODES
C00007 00004	SWITCHES
C00008 00005	File control Switches F,T,P
C00009 00006	Input control switches  G,Y,M,E,D,V,X,I,N
C00015 00007	Output formatting switches H,Q,A,O,S,J,U,B,C,R,Z
C00021 00008	Run time tty message switches, and kounters      L,W,K
C00023 00009	FILES
C00025 00010	Sample Run
C00026 ENDMK
C⊗;
FOLMRG is a program for reformating FOL input and output files.  It has 
the ability to justify proofs, count statements, prepare for pub output, 
and rename identifiers.

Execution of the program is controled by the settings of several switches.
Additionally, for ease of operation, the are several modes, each of which
automatically selects a convient and related group of switches.

The program usually expects two input files: a FOL command file, and a file
created by a SHOW PROOF on the proof that the command file generated.  It 
is possible to run the program on a single proof file (I switch), or if 
the program is being used solely for renaming identifiers in which case 
any text file will do (the YO switch). 

MODES

When execution of the program begins, the user is confronted with a choice 
of modes.  Selection of a mode sets some switches; more switches can be added 
later.

The user wishing a fast and dirty pub preparation can merely request one of 
the PUB modes, express no desire to set other switches, and proceed to tell 
FOLMRG which files to process.

There are currently four modes

F       FOL mode.  This is the standard full size FOL publication mode.  The
	proof is printed in medium size type.  Different fonts are used for 
	FOL commands and responses, and the output looks like a user-FOL
	interactive session.  It is equivalent to setting the switches:
	M,E,H,JF=70,U,B,X,C=%6,R=%7.  The resulting file is ready for PUB.

A       FOL appendix mode.  This is the standard way to create compact records
	of FOL proofs.  It uses smaller type but you get more to the page.  It
        acts like switches M,E,H,JF=108,U,B,X.  The result is ready for PUB.

P       Proof file only.  When you want to reformat a file created by FOLs 
	SHOW PROOF command.  It lets you get a different linelength, rename 
	variables, or, collect frequency statistics on the different FOL 
	commands you used.  Sets the switches Z=,Y=,I

R       Renaming only.  When you want to use this program to rename identifiers
	in a file.  Works on non-FOL files, too.

If one of the PUB modes is requested, the users line editor is loaded with a
request to pub after program execution.  Any letter other than F,A,P or R is
ignored.  In any case, you're asked if you want to set any other switches.

The headers produced by the F and A options are, respectively, are found in
the files FOLMAC.DAT[MRG,REF] and APPMAC.DAT[MRG,REF].
SWITCHES

The are several classes of switches.  Successive pages describe the switches
in each class.
File control Switches F,T,P

Certain switches control where to start and stop reading files.

    F=λ     fetch From mark λ.  Start processing the FOL file when the statement
            MARK  λ; is encountered.  λ can be, of course, any FOL token.

    T=λ     fetch To mark λ.  Stop program processing when the mark λ is reached.

An alternate way of skiping part of a file involves the P switches

    PF=n    start reading Fol file at Page n
    PP=n    start reading Proof file at Page n
Input control switches  G,Y,M,E,D,V,X,I,N

Several switches control processing of the FOL file input.  The switches
request certain conversions of and deletions from the input stream.

The first four switches in this group request the deletion or inclusion
of certain characters from the FOL input file.

    M       print the Marks in the FOL input file.  If M is not set,
	    then all MARK commands are ignored.

    E       print the declarative and administrative commands in file.
	    Same as M, except for declares, shows, attachments, mg, etc.

    D       Delete all comments.  Both kind of comments (COMMENT and %)
	    are recognized.  If this switch is not requested, comments will
	    be put in the output file.

    V       don't print formfeeds seen in the FOL file.  Otherwise, the program
	    will convert any formfeed in the FOL input file to an appropriate
	    formfeed on output.  The program will avoid spliting a single 
	    command onto two different pages, however.

The next set of switches request certain conversions be done on the input
files before further processing.

    X       All tabs are converted to the character `\'.  Additionally,
            all `\'s already in the file are PUB quoted.  Note that if you
            specify a set of PUB quote characters after invoking the X
            switch, then \ will not necessarily be quoted.

    YA=file Do the renamings requested in `file'
    YO=file Do the renamings requested in `file'.  Do no other processing.
	    The Y switches are used for renaming the identifiers in a file.
	    The argument file has a list of identifier changes, one
	    per line, the first the old word, the second, its replacement.
	    The two words are separated by a space.  Substitution pairs
	    must exist one per line.  Formfeeds are ignored on input, but
	    the file may contain no other information (such as blank lines
	    or ETV directory pages).  Using a Y option slows the program
	    to about 40% of its original speed.  If the YO option is requested,
	    no other switches are considered, the program merely does identifier
	    substitution.  However, the input file is no longer assumed to
	    be a FOL input file; any file may be used.  Hence, FOLMRG may
	    be used as a general identifier substitution program.

Other input selection switches.

    I       Formatting only one input file.  If you want to take a proof
	    file, and process it with the other options, (that is, treat the
	    FOL generated commands as coming from the file), use the I option.
            You will be asked for only one input file.

    N       assumptions involving Ntuples are made (so <> are not relationals)
            FOLMRG does not look at/know about the declarations made in the
	    FOL proof.  Not knowing the types of identifiers implies an ambiguity
	    in determining the number of statements generated by a single fol
	    command.  To wit, ASSUME A < B , C >; might generate either a
	    single line refering to the action of the prefix predicate A
	    when confronted with the tuple argument <B,C>, or it might
	    generate the two proof steps, A<B, and C>, where > is then obviously
	    an individual.  The default is the former, but if your declarations
	    are obscure enough, you might appreciate the latter.  If none
	    of this makes sense to you, you probably don't need the N switch.

    G       if you find a fetch command, Get that file, and transcribe it 
	    verbatim.  This switch doesn't exactly act this way.  In fact, 
	    it hasn't yet been implemented.  If anybody really wants it, 
	    however, I might find the time to implement full processing of
	    fetch commands.
Output formatting switches H,Q,A,O,S,J,U,B,C,R,Z

These switches detail the reformating actions

In step changes.

    A=c     PUB quote character is to be (default = α)(Alpha character)
	    Whenever FOLMRG has to quote a PUB command character, it uses c.

    Q=s     sets the set of PUB quote chars to s (default = α%{ )
	    Whenever one of the PUB quote characters is encountered in output
	    stream, it is quoted with a the pub quote character.  This does
	    not include, of course, pub command characters inserted by FOLMRG

    O       don't quote periods in column One
	    Unless the O option is invoked, FOLMRG will
	    PUB quote (alphachar) every period in column one.


    Z=s     Print Ztring s before every command (default=`*****')
    C=%c    switch to font c in Commands (default NULL)
    R=%d    switch to font d in Responses (default NULL) (% is font switch char)
	    Every line of command from the FOL file is surrounded on output,
	    by three strings.  The string s, followed by the characters %c,
	    proceed each line.  The chacters %d end the line.  The s string
	    is abbrieviated to its first character on all lines of a FOL
	    command other than the first.  This permits switching to another 
	    font for the FOL commands.
	    
Justification switches
    JF{=n}  do simple justifying, of lines of length n (JustFill)
    JU{=n}  do complex justifying (don't split identifiers) (JUstify)
	    FOLMRG knows of two ways to justify the proof output.
	    Either every line can be forced to the same length (JF),
	    which involves spliting identifiers and sticking percent
	    signs at the end of every line (this is the way the stuff
	    looks when it comes out of FOL), or the program can keep
            your identifiers together on the same line.  This results in
	    a ragged right margin, but virtually no percent characters.
	    In either case, n is the length of the longest of the 
	    resulting lines.  If the =n is omitted, 108 is used for the
	    linelength.  Don't try asking for a linelength of less than 5;
	    it won't work.
    U       jUstify the FOL commands, too.  FOLMRG will not remove
	    the interior CRLF's from for FOL commands, but if a line of
	    FOL input is longer than linelength, using the U switch will
	    compact it.


Output spacing
    H       Keep commands and steps togetHer on the same page
	    Puts PUB `GROUP' and `APART' commands around rules of inference
	    and their generated steps.  Also around axiom definitions.

    SA=n    number of lines to Skip between command and answer (default = 0)(intrA)
    SR=n    number of lines to Skip between proof steps (default = 1)(inteR)
    SW=n    insert an additional blank line every n steps (default =10E6)(Skip When)
    SF=n    insert an additional page mark every n steps (default =10E6)(Skip When)
	    The skip switches control the regular insertions of blank lines
	    in the output.  SA blank lines are inserted between a command and its
	    response, SR between the proof steps.  An additional blank line
	    is inserted every SW steps, and a formfeed, every SF steps.

    B       Print # in every Blank line.  Also, add # to the PUB quoted chars.
	    The B switch controls what is printed on blank lines.  If B
	    is invoked, then every blank line contains the PUB space character,
	    `#'.  Every # in the text is pub quoted.  This switch helps PUB
	    get the page size correct when using different size fonts.
Run time tty message switches, and kounters      L,W,K

Run time messages.
    L       don't print line numbers of statements processed
	    Unless you invoke the L switch, FOLMRG will print the line number
	    of each proof step it processes.  If you tired of having your
	    screen filled with little digits, try L.

    W       don't Warn me when the FOL command is not the same as the proof command
	    FOLMRG tries to warn you if certain unusual conditions occur.
	    Particularly, unterminated comments, and FOL commands that
	    do not match the proof file command provoke messages.  If you
	    don't want these messages, use the W switch.

Counters
    K       Kount the FOL command frequency
	    FOLMRG has a facility for counting the frequency of the
	    FOL commands in your proof.  If you use the K switch, you
	    will be asked for a file for the results.
	    FOLMRG knows the state of the current FOL commands from the
	    information in HASH.DAT[MRG,REF].  Don't change this file
	    unless you know what you're doing.
FILES

FOLMRG will normally ask for the names of three files, a FOL commands 
input file, a PROOF input file, and an OUTPUT file. If the K switch 
is invoked, a file name for counter output is also requested.   A Y 
option likewise requires the name of a data file.  If the I switch 
is called, FOLMRG requests only one primary input file.

If the first file request is answered <filename>.*, then the input 
files are presumed to be:

FOL command file	<filename>.FOL
shown PROOF file	<filename>.PRF
primary output file	<filename>.OUT
file for counters	<filename>.KNT
     (if any)

Note:  you cannot respond  FOOBAZ.*[FOO,BAZ]
Sample Run

.R FOLMRG
<display>
MODE?p
<display is cleared>

Do you want to set any of the switches yourself?y
<display>

Switches?T=MARKEND,jf=50,u,b,x,r=%7,z=?????,k
<display is cleared>
FOL input file? FOOBAZ.FOL
PROOF input file? BAZFOO.PRF
Output file? PUTOUT.OUT

1 2 3 4 5 6 7  File for counters? CUMQAT.KNT
Finished

End of SAIL execution.